Finding errors in hardware designs is a difficult problem that often requires searches based on binary decision diagrams (BDDs). However, current BDD approaches are typically unstable, inefficient, or both.